# library of macro's representing name-mangled polymorphic functions, does not contain actual Twelf code! 
def defdecl(defn, decl, dodecl)
if dodecl then
  decl
else
  defn
end
end


%%<-------- CONS-LISTS
def list(tp, dodecl=false) 
list2(tp, tp, dodecl)
end


def list2(tp, n, dodecl=false) 
defn = <<EODEF
list@#{n} : nat -> type.
nil@#{n}  : list@#{n} 0.
cons@#{n} : #{tp} -> list@#{n} N -> list@#{n} (s N).
EODEF

decl =  <<EODECL
% partial Nth for lists of #{tp} 
 nth_opt_#{n} : nat -> list@#{n} N -> #{tp} -> type.
 %mode nth_opt_#{n} +N +CL -C.
 %name nth_opt_#{n} CNTH cnth.

 nth_sz_#{n}: nth_opt_#{n} 0 (cons@#{n} C CS) C.
 nth_sn_#{n}: nth_opt_#{n} N CS C -> nth_opt_#{n} (s N) (cons@#{n} D CS) C.

% Append for lists of #{tp} 
 append@#{n} : list@#{n} N1 -> list@#{n} N2 -> list@#{n} N3 -> sum N1 N2 N3 -> type.
 % mode append@#{n} +CNL1 +CNL2 -CNL3 -PL.

 append@#{n}/nil  : append@#{n} nil@#{n} CS CS PS <- sum-ident _ PS.

 append@#{n}/cons : append@#{n} (cons@#{n} CN CS1) CS2 (cons@#{n} CN CS3) PL-inc
                         <- append@#{n} CS1 CS2 CS3 PL
                         <- sum-commute PL PL'
                         <- sum-inc PL' PL-inc'
                         <- sum-commute PL-inc' PL-inc.

 append@#{n} : list@#{n} N1 -> list@#{n} N2 -> list@#{n} N3 -> type.
 % mode append@#{n} +CNL1 +CNL2 -CNL3.

 append_simp@#{n} : list@#{n} N1 -> list@#{n} N2 -> list@#{n} N3 ->  type.
 append_simp@#{n}/nil  : append_simp@#{n} nil@#{n} CS CS.

 append_simp@#{n}/cons : append_simp@#{n} (cons@#{n} CN CS1) CS2 (cons@#{n} CN CS3)
                         <- append_simp@#{n} CS1 CS2 CS3.

 % worlds () (append@#{n} CS1 CS2 CS3 PL).
 % terminates CS1 (append@#{n} CS1 CS2 CS3 PL).
 % unique append@#{n} +CS1 +CS2 -1CS3 -1PL.
 % covers append@#{n} +CS1 +CS2 -CS3 -PL.
 % total CS1 (append@#{n} CS1 CS2 CS3 PL).
EODECL

defdecl(defn, decl, dodecl) 
end 

def list_indexed(tp, dodecl=false) 
list2_indexed(tp, tp, dodecl)
end


def list2_indexed(tp, n, dodecl=false) 
defn = <<EODEF
list@#{n} : nat -> type.
nil@#{n}  : list@#{n} 0.
cons@#{n} : #{tp} _ -> list@#{n} N -> list@#{n} (s N).
EODEF

decl =  <<EODECL
% partial Nth for lists of #{tp} 
 nth_opt_#{n} : nat -> list@#{n} N -> #{tp} _ -> type.
 %mode nth_opt_#{n} +N +CL -C.
 %name nth_opt_#{n} CNTH cnth.

 nth_sz_#{n}: nth_opt_#{n} 0 (cons@#{n} C CS) C.
 nth_sn_#{n}: nth_opt_#{n} N CS C -> nth_opt_#{n} (s N) (cons@#{n} D CS) C.

% Append for lists of #{tp} 
 append_#{n} : list@#{n} N1 -> list@#{n} N2 -> list@#{n} N3 -> sum N1 N2 N3 -> type.
 %mode append_#{n} +CNL1 +CNL2 -CNL3 -PL.

 append_#{n}_nil@#{n}  : append_#{n} nil@#{n} CS CS PS <- sum-ident _ PS.

 append_#{n}_cons@#{n} : append_#{n} (cons@#{n} CN CS1) CS2 (cons@#{n} CN CS3) PL-inc
                         <- append_#{n} CS1 CS2 CS3 PL
                         <- sum-commute PL PL'
                         <- sum-inc PL' PL-inc'
                         <- sum-commute PL-inc' PL-inc.

 % worlds () (append_#{n} CS1 CS2 CS3 PL).
 % terminates CS1 (append_#{n} CS1 CS2 CS3 PL).
 % unique append_#{n} +CS1 +CS2 -1CS3 -1PL.
 % covers append_#{n} +CS1 +CS2 -CS3 -PL.
 % total CS1 (append_#{n} CS1 CS2 CS3 PL).
EODECL

defdecl(defn, decl, dodecl) 
end 


def splice(tp, n=tp)
res = <<EOSTR
% focussing into a list of arguments
splice_fun_#{n} : list@#{n} M -> list@#{n} N -> (#{tp} -> list@#{n} O) -> sum M (s N) O -> type.
%mode splice_fun_#{n} +CS1 +CS2 -CS3 -PL.

splice_fun_#{n}/nil : splice_fun_#{n} nil@#{tp} B ([x] (cons@#{tp} x B)) PS
                  <- sum-ident _ PS'
                  <- sum-commute PS' PS.

splice_fun_#{n}/cons : splice_fun_#{n} (cons@#{tp} A AS) BS ([x] (cons@#{tp} A (ASBS x))) (PS-inc : sum (s NAS) (s NBS) (s N))
                  <- splice_fun_#{n} AS BS ASBS (PS: sum NAS (s NBS) N)
                  <- sum-commute PS PS'
                  <- sum-inc PS' PS'-inc
                  <- sum-commute PS'-inc PS-inc.

%worlds () (splice_fun_#{n} CS1 CS2 CS3 PL).
%terminates CS1 (splice_fun_#{n} CS1 CS2 CS3 PL).
% unique splice_fun_#{n} +CS1 +CS2 -1CS3 -1PL.
%covers splice_fun_#{n} +CS1 +CS2 -CS3 -PL.
%total CS1 (splice_fun_#{n} CS1 CS2 CS3 PL).
EOSTR
end


def lookup(tp, eq, neq, n=tp)
res = <<EOSTR
% Lookup requires neq@#{n} and eq@#{n}

neq@#{n} : #{tp} -> #{tp} -> type. % Has to be defined by client
#{neq}
%mode neq@#{n} +X1 +X2.
% worlds () (neq@#{n} X1 X2).
% terminates {X1 X2} (neq@#{n} X1 X2).

eq@#{n} : #{tp} -> #{tp} -> type. % Has to be defined by client
#{eq}
eq@#{n}-refl : eq@#{n} X X.
%mode eq@#{n} +X1 +X2.
% worlds () (eq@#{n} X1 X2).
% terminates {X1 X2} (eq@#{n} X1 X2).

in_#{n} : #{tp} -> list@#{n} N -> type.
%name in_#{n} IN in.
%mode in_#{n} +X +XS.

in_#{n}_cons1 :   {XS: (list@#{n} N)} eq@#{n} X1 X2 ->
                % -----------------------------------------------------------------
                  in_#{n} X1 (cons@#{n} X2 XS).

in_#{n}_cons2 : {XS: (list@#{n} N)} neq@#{n} X1 X2 ->
                  in_#{n} X1 XS ->
                % -----------------------------------------------------------------
                  in_#{n} X1 (cons@#{n} X2 XS).

% worlds () (in_#{n} X XS).
% terminates XS (in_#{n} X XS).

not_in_#{n} : #{tp} -> list@#{n} N -> type.
%name not_in_#{n} NIN nin.
%mode not_in_#{n} +X +XS.

not_in_#{n}_nil : not_in_#{n} X1 (nil@#{n}).

not_in_#{n}_cons : {XS: (list@#{n} N)} neq@#{n} X1 X2 ->
                   not_in_#{n} X1 XS ->
                % -----------------------------------------------------------------
                  not_in_#{n} X1 (cons@#{n} X2 XS).

% worlds () (not_in_#{n} X XS).
% terminates XS (not_in_#{n} X XS).
EOSTR
end


def lift1_list(orig, tp, lifted) 
res = <<EOSTR
nil@#{lifted} : #{lifted} nil@#{tp}.
cons@#{lifted} : #{lifted} (cons@#{tp} X XS)
               <- #{lifted} XS
               <- #{orig} X.
EOSTR
end


def lift1_list_postfix(orig, tp, lifted) 
res = <<EOSTR
nil@#{orig} : nil@#{tp} #{lifted}.
cons@#{orig} : (cons@#{tp} X XS) #{lifted}
               <- XS #{lifted}
               <- X #{orig}.
EOSTR
end


def lift2_list_arg2(orig, tp, lifted) 
res = <<EOSTR
nil@#{lifted} : #{lifted} _ nil@#{tp}.
cons@#{lifted} : #{lifted} A (cons@#{tp} X XS)
               <- #{lifted} A XS
               <- #{orig} A X.
EOSTR
end


def lift2_list_arg3(orig, tp, lifted) 
res = <<EOSTR
nil@#{lifted} : #{lifted} _ _ nil@#{tp}.
cons@#{lifted} : #{lifted} A B (cons@#{tp} X XS)
               <- #{lifted} A B XS
               <- #{orig} A B X.
EOSTR
end


def lift2_list(orig, tpa, tpb, lifted) 
res = <<EOSTR
nil@#{lifted} : #{lifted} nil@#{tpa} nil@#{tpb}.
cons@#{lifted} : #{lifted} (cons@#{tpa} X XS) (cons@#{tpb} Y YS)
               <- #{lifted} XS YS
               <- #{orig} X Y.
EOSTR
end


def lift2_list_infix(orig, tpa, tpb, lifted) 
res = <<EOSTR
nil@#{orig} : nil@#{tpa} #{lifted} nil@#{tpb}.
cons@#{orig} : (cons@#{tpa} X XS) #{lifted} (cons@#{tpb} Y YS)
               <- XS #{lifted} YS
               <- X #{orig} Y.
EOSTR
end

%%--------->

%%<-------- APPEND LISTS
def append_list(tp, dodecl=false) 
append_list2(tp, "append_#{tp}", dodecl)
end


def append_list2_not_indexed(tp, n, dodecl=false) 
defn = <<EODEF
list@#{n} : type.
nil@#{n}  : list@#{n}.
cons@#{n} : #{tp} -> list@#{n} -> list@#{n}.
append_#{tp} : list@#{n} -> list@#{n} -> list@#{n}.
EODEF

decl =  <<EODECL
isomorphic_list@#{n} : {AS: list@#{n}} {AS': list@#{n}} type.
%mode isomorphic_list@#{n} +AS +AS'.
isomorphic_list@#{n}-refl : isomorphic_list@#{n} AS AS.
isomorphic_list@#{n}-todo : {AS: list@#{n}} {AS': list@#{n}} isomorphic_list@#{n} AS AS'.

iso_list@#{n} : {AS: list@#{n}} {AS': list@#{n}} isomorphic_list@#{n} AS AS' -> type.
%mode iso_list@#{n} -AS +AS' -ISO.

iso_list@#{n}/refl  : iso_list@#{n} AS AS isomorphic_list@#{n}-refl.
iso_list@#{n}/cons  : iso_list@#{n} (cons@#{n} A AS2) (append_#{tp} nil@#{n} (cons@#{n} A AS2)) (isomorphic_list@#{n}-todo _ _).
iso_list@#{n}/cons2  : iso_list@#{n} (cons@#{n} B BS) (append_#{tp} (cons@#{n} B BS') (cons@#{n} A AS2)) (isomorphic_list@#{n}-todo _ _)
   <- iso_list@#{n} BS (append_#{tp} BS' (cons@#{n} A AS2)) _.
iso_list@#{n}/appendX  : iso_list@#{n} (append_#{tp} XS YS) (append_#{tp} AS1 (cons@#{n} A (append_#{tp} AS2 YS))) (isomorphic_list@#{n}-todo _ _)
   <- iso_list@#{n} XS (append_#{tp} AS1 (cons@#{n} A AS2)) _.
iso_list@#{n}/appendY  : iso_list@#{n} (append_#{tp} XS YS) (append_#{tp} (append_#{tp} XS AS1) (cons@#{n} A AS2)) (isomorphic_list@#{n}-todo _ _)
   <- iso_list@#{n} YS (append_#{tp} AS1 (cons@#{n} A AS2)) _.

%worlds () (iso_list@#{n} _ _ _).
%covers iso_list@#{n} -AS +AS' -ISO.

EODECL

defdecl(defn, decl, dodecl) 
end 

def bla()
bla = <<EOBLA
% append for append lists of #{tp}, if input lists only consisted of nil/cons, output will also be strictly nil/cons
append_#{n} : list@#{n}  -> list@#{n}  -> list@#{n} -> type.
%mode append_#{n} +CNL1 +CNL2 -CNL3 .

append_#{n}_nil@#{n}  : append_#{n} nil@#{n} CS CS .

append_#{n}_cons@#{n} : append_#{n} CS1 CS2 CS3  ->
                          % ----------------------------------------------------------
                          append_#{n} (cons@#{n} CN CS1) CS2 (cons@#{n} CN CS3) .

append_#{n}_append_#{n} : append_#{n} (append_#{tp} AS BS) CS ABCS 
                           <- append_#{n} BS CS BCS 
                           <- append_#{n} AS BCS ABCS.


%worlds () (append_#{n} CS1 CS2 CS3 ).
%terminates CS1 (append_#{n} CS1 CS2 CS3 ).
%unique append_#{n} +CS1 +CS2 -1CS3 .
%covers append_#{n} +CS1 +CS2 -CS3 .
%total CS1 (append_#{n} CS1 CS2 CS3).


normalise_list@#{n} : {AS: list@#{n}} {AS': list@#{n}} isomorphic_list@#{n} AS AS' -> type.
%mode normalise_list@#{n} +AS -AS' -ISO.
normalise_list@#{n}-nil : normalise_list@#{n} nil@#{n} nil@#{n} (isomorphic_list@#{n}-todo _ _).
normalise_list@#{n}-cons : normalise_list@#{n} (cons@#{n} A AS) (cons@#{n} A AS') (isomorphic_list@#{n}-todo _ _)
                                <- normalise_list@#{n} AS AS' _.
normalise_list@#{n}-app : normalise_list@#{n} (append_#{tp} AS1 AS2) AS12 (isomorphic_list@#{n}-todo _ _)
                                <- normalise_list@#{n} AS1 AS1' _
                                <- normalise_list@#{n} AS2 AS2' _
                                <- append_#{n} AS1' AS2' AS12. % TODO

%worlds () (normalise_list@#{n} _ _ _).
%total {AS1} (normalise_list@#{n} AS1 AS2 ISO).
EOBLA
end


def append_list2(tp, n, dodecl=false) 
defn = <<EODEF
list@#{n} : nat -> type.
nil@#{n}  : list@#{n} 0.
cons@#{n} : #{tp} -> list@#{n} N -> list@#{n} (s N).
append_#{tp} : list@#{n} N -> list@#{n} M -> sum N M NM -> list@#{n} NM.
EODEF

decl =  <<EODECL
isomorphic_list@#{n} : {AS: list@#{n} N} {AS': list@#{n} N} type.
%mode isomorphic_list@#{n} +AS +AS'.
isomorphic_list@#{n}/refl : isomorphic_list@#{n} AS AS.
isomorphic_list@#{n}/nil : isomorphic_list@#{n} (AS: list@#{n} 0) (AS': list@#{n} 0).
isomorphic_list@#{n}/todo : {AS: list@#{n} N} {AS': list@#{n} N} isomorphic_list@#{n} AS AS'.

iso_list@#{n} : {AS: list@#{n} N} {AS': list@#{n} N} isomorphic_list@#{n} AS AS' -> type.
%mode iso_list@#{n} -AS +AS' -ISO.

% TODO: deterministic
iso_list@#{n}/refl   : iso_list@#{n} AS AS isomorphic_list@#{n}/refl.
iso_list@#{n}/appnil : iso_list@#{n} AS (append_#{tp} nil@#{n} AS _) (isomorphic_list@#{n}/todo _ _).
iso_list@#{n}/cons   : iso_list@#{n} (cons@#{n} B BS) (append_#{tp} (cons@#{n} B BS') (cons@#{n} A AS2) PL1-inc) (isomorphic_list@#{n}/todo _ _)
   <- sum-commute PL1-inc PL1-inc'
   <- sum-inc' PL1' PL1-inc'
   <- sum-commute PL1' PL1
   <- iso_list@#{n} BS (append_#{tp} BS' (cons@#{n} A AS2) PL1) _.

iso_list@#{n}/appendX  : iso_list@#{n} (append_#{tp} XS YS PS_ASBS) 
                                           (append_#{tp} AS BS PS_ASBS) (isomorphic_list@#{n}/todo _ _)
  <- iso_list@#{n} XS AS _
  <- iso_list@#{n} YS BS _ .

% TODO: more cases...


%worlds () (iso_list@#{n} _ _ _).
%covers iso_list@#{n} -AS +AS' -ISO.
EODECL

defdecl(defn, decl, dodecl) 
end 

def lift1_append_list(orig, tp, lifted) 
res = <<EOSTR
#{lifted}-nil : #{lifted} nil@append_#{tp}.
#{lifted}-cons : #{lifted} (cons@append_#{tp} X XS)
               <- #{orig} X
               <- #{lifted} XS.
#{lifted}-append : #{lifted} (append_#{tp} XS YS _)
               <- #{lifted} XS
               <- #{lifted} YS.
EOSTR
end



# lift over an append_list (of tpa's) and a list (of tpb's)
def lift2_append_list_infix(orig, tpa, tpb, lifted) 
res = <<EOSTR
#{lifted}-nil : nil@append_#{tpa} #{lifted} nil@#{tpb}.
#{lifted}-cons : (cons@append_#{tpa} X XS) #{lifted} (cons@#{tpb} Y YS)
               <- X #{orig} Y
               <- XS #{lifted} YS.
#{lifted}-append : (append_#{tpa} (cons@append_#{tpa} X XS) XS2 PL-inc) #{lifted} (cons@#{tpb} Y YS)
               <- X #{orig} Y
               <- sum-commute PL-inc PL-inc'
               <- sum-inc' PL PL-inc'
               <- (append_#{tpa} XS XS2 PL) #{lifted} YS.
EOSTR
end

%%--------->

%%<-------- OPTIONS
def opt(tp, dodecl=false) 
defn = <<EODEF
opt@#{tp} : type.
 none@#{tp} : opt@#{tp}.
 some@#{tp} : #{tp} -> opt@#{tp}.
EODEF

decl = <<EODECL
EODECL
defdecl(defn, decl, dodecl) 
end 

def opt_indexed(tp, index, dodecl=false) 
defn = <<EODEF
opt@#{tp} : #{index} -> type.
 none@#{tp} : opt@#{tp} _.
 some@#{tp} : #{tp} I -> opt@#{tp} I.
EODEF

decl = <<EODECL
EODECL
defdecl(defn, decl, dodecl) 
end 
%%---------->

def pair(tpa, tpb, dodecl=false) 
defn = <<EODEF
pair_#{tpa}_#{tpb} : type.
 mkpair_#{tpa}_#{tpb} : {A: #{tpa}} {B: #{tpb}} pair_#{tpa}_#{tpb}.
EODEF

decl = <<EODECL
EODECL
defdecl(defn, decl, dodecl) 
end 

def binds_append_list(tpa, ntpa, tpb, ntpb=tpb, dodecl=false) 
defn = <<EODEF
binds_#{tpa}_#{tpb} : list@#{ntpb} N -> type.
 body_#{tpa}_#{tpb} : #{tpa} -> binds_#{tpa}_#{tpb} nil@#{ntpb}.
 bind_#{tpa}_#{tpb} : {T:#{tpb}} (#{tpa} -> binds_#{tpa}_#{tpb} TS) -> binds_#{tpa}_#{tpb} (cons@#{ntpb} T TS).
EODEF

decl = <<EODECL
% Given a list of binders and a list of actual arguments, perform the substitutions
subst_#{tpa}_#{tpb} : binds_#{tpa}_#{tpb} (CS:list@#{ntpb} N) -> list@#{ntpa} N -> #{tpa} -> type.
%mode subst_#{tpa}_#{tpb} +BT +TL -T1.

subst_body_#{tpa}_#{tpb} : subst_#{tpa}_#{tpb} (body_#{tpa}_#{tpb} E) nil@#{ntpa} E.

%% peel away one argument, E1, and the binder BE, apply and "recurse"
subst_bind_#{tpa}_#{tpb} : subst_#{tpa}_#{tpb} (BE E1) EL E2 ->
           % --------------------------------------------------
             subst_#{tpa}_#{tpb} (bind_#{tpa}_#{tpb} _ ([x:#{tpa}] BE x)) (cons@#{ntpa} E1 EL) E2.

%worlds () (subst_#{tpa}_#{tpb} BE EL E1).
%unique subst_#{tpa}_#{tpb} +BE +EL -1E1.
% TODO why does this work in fj.elf but not here:
% total BE (subst_#{tpa}_#{tpb} BE EL E1).
EODECL
defdecl(defn, decl, dodecl) 
end 

def binds_indexed1(tpa, tpb, dodecl=false) 
defn = <<EODEF
binds_#{tpa}_#{tpb} : list@#{tpb} N -> type.
 body_#{tpa}_#{tpb} : #{tpa} _ -> binds_#{tpa}_#{tpb} nil@#{tpb}.
 bind_#{tpa}_#{tpb} : {T:#{tpb}} (#{tpa} _ -> binds_#{tpa}_#{tpb} TS) -> binds_#{tpa}_#{tpb} (cons@#{tpb} T TS).
EODEF

decl = <<EODECL
% Given a list of binders and a list of actual arguments, perform the substitutions
subst_#{tpa}_#{tpb} : binds_#{tpa}_#{tpb} (CS:list@#{tpb} N) -> list@#{tpa} N -> #{tpa} _ -> type.
%mode subst_#{tpa}_#{tpb} +BT +TL -T1.

subst_body_#{tpa}_#{tpb} : subst_#{tpa}_#{tpb} (body_#{tpa}_#{tpb} E) nil@#{tpa} E.

%% peel away one argument, E1, and the binder BE, apply and "recurse"
subst_bind_#{tpa}_#{tpb} : subst_#{tpa}_#{tpb} (BE E1) EL E2 ->
           % --------------------------------------------------
             subst_#{tpa}_#{tpb} (bind_#{tpa}_#{tpb} _ ([x:#{tpa} _] BE x)) (cons@#{tpa} E1 EL) E2.

% worlds () (subst_#{tpa}_#{tpb} BE EL E1).
% unique subst_#{tpa}_#{tpb} +BE +EL -1E1.
% TODO why does this work in fj.elf but not here:
% total BE (subst_#{tpa}_#{tpb} BE EL E1).
EODECL
defdecl(defn, decl, dodecl) 
end 

def binds(tpa, tpb, dodecl=false) 
defn = <<EODEF
binds_#{tpa}_#{tpb} : list@#{tpb} N -> type.
 body_#{tpa}_#{tpb} : #{tpa} -> binds_#{tpa}_#{tpb} nil@#{tpb}.
 bind_#{tpa}_#{tpb} : {T:#{tpb}} (#{tpa} -> binds_#{tpa}_#{tpb} TS) -> binds_#{tpa}_#{tpb} (cons@#{tpb} T TS).
EODEF

decl = <<EODECL
% Given a list of binders and a list of actual arguments, perform the substitutions
subst_#{tpa}_#{tpb} : binds_#{tpa}_#{tpb} (CS:list@#{tpb} N) -> list@#{tpa} N -> #{tpa} -> type.
%mode subst_#{tpa}_#{tpb} +BT +TL -T1.

subst_body_#{tpa}_#{tpb} : subst_#{tpa}_#{tpb} (body_#{tpa}_#{tpb} E) nil@#{tpa} E.

%% peel away one argument, E1, and the binder BE, apply and "recurse"
subst_bind_#{tpa}_#{tpb} : subst_#{tpa}_#{tpb} (BE E1) EL E2 ->
           % --------------------------------------------------
             subst_#{tpa}_#{tpb} (bind_#{tpa}_#{tpb} _ ([x:#{tpa}] BE x)) (cons@#{tpa} E1 EL) E2.

% worlds () (subst_#{tpa}_#{tpb} BE EL E1).
% unique subst_#{tpa}_#{tpb} +BE +EL -1E1.
% TODO why does this work in fj.elf but not here:
% total BE (subst_#{tpa}_#{tpb} BE EL E1).
EODECL
defdecl(defn, decl, dodecl) 
end 